Model checking is a method of formal verification that is gaining in popularity as a tool for use in designing complex systems, such as integrated circuits. The method is described generally by Clarke et al. in Model Checking (MIT Press, 1999), which is incorporated herein by reference.
To perform model checking of the design of a device, a user reads the definition and functional specifications of the device and then, based on this information, writes a set of properties {φ} (also known as a specification) that the design is expected to fulfill. The properties are written in a suitable specification language for expressing temporal logic relationships between the inputs and outputs of the device. Such languages are commonly based on Computation Tree Logic (CTL). A hardware model M (also known as an implementation) of the design, which is typically written in a hardware description language, such as VHDL or Verilog, is then tested to ascertain that the model satisfies all of the properties in the set, i.e., that M |=φ, under all relevant input sequences. Such testing is a form of reachability analysis.
One of the most useful features of model checking is its ability, when a property φ is found to be false on M, to construct a sequence of states and transitions (a path) that leads to the problematic state of the design. This path is called a counterexample. It can be used by the engineer in understanding and remedying the design defect that led to the failure of the model.
Model checking is typically carried out automatically using a symbolic model checking program, such as SMV, as described, for example, by McMillan in Symbolic Model Checking (Kluwer Academic Publishers, 1993), which is incorporated herein by reference. A number of practical model checking tools are available, among them RuleBase, developed by IBM Corporation. This tool is described by Beer et al. in “RuleBase: an Industry-Oriented Formal Verification Tool,” in Proceedings of the Design Automation Conference DAC'96 (Las Vegas, Nev., 1996), which is incorporated herein by reference.
Symbolic CTL model checking as described by McMillan involves computing the transition-relation (TR) of the model, and then applying the model checking algorithm to verify a specified formula. In many cases, the full TR is too big to be computed. This problem is addressed by Beer et al., in “On-the-fly Model Checking of RCTL Formulas,” Proceedings of the Tenth International Conference on Computer Aided Verification (CAV 1998), which is incorporated here in by reference. In this paper, the authors describe a technique for solving CTL formulas of the form AG(p), wherein p is a Boolean expression. An AG(p) formula states that p is true in every reachable state of the model. Therefore, to disprove this formula, it is sufficient to find one reachable state in which p is false. In the context of the present patent application and in the claims, such a state is referred to as a target state. It may also be called a “bad” state, as it violates the specified formula.
If S is the set of states in which p is false, then in order to find a “bad” state, it is necessary only to intersect S with the set of reachable states R of the model, and check that the intersection is not empty. Finding this intersection is computationally easy, and therefore can be performed on the fly, i.e., after each iteration of the reachability analysis. If the intersection of S and R is found at any point to be non-empty, the process is stopped, and AG(p) is false. Otherwise, the process continues and terminates when the entire reachable state space has been computed, so that AG(p) is shown to be true. Thus, this method eliminates the large expenditure of computation resources needed to compute the full transition relation. Furthermore, since counterexamples are produced as soon as the target state is found, only a portion of the reachable state space must be computed when the formula fails, saving even more time and memory space.
The on-the-fly model checking procedure is shown formally in Table I below:
TABLE ION-THE-FLY MODEL CHECKING1reachable = new = initialStates;2i = 0;3while ((new ≠ Ø)&&(new ∩ p = Ø)) {4Si = new;5i = i+1;6next = nextStateImage (new)7new = next \ reachable;8reachable = reachable ∪ next;9}10if (new = Ø) {11print “formula is true in the model”;12return;13}Here the “&&” operator represents logical conjunction, and the function “nextStateImage(new)” returns the states that are reached in one cycle of the system transition relation beginning from the states in {new}.
If it is found at any cycle of the above process that new ∩φp≠Ø, the model checker informs the user that the formula AG(p) is false for the model in question. Typically, the model checker goes on to compute a counterexample, by finding a trace back through the state space from one of the states in the intersection region {new ∩φp} to one of the initial states. A similar procedure can be used to find a “witness,” or positive example, demonstrating fulfillment of a formula EF(p). This latter formula states that there exists some path through the state space of the model to some state on which p is true. It is the dual of AG(φp). In this case, the target states are those in which p is true.
In the above-mentioned article, Beer et al. describe a technique for translating many CTL formulas conveniently into state machines having an error state. Such formulas can then be verified by on-the-fly model checking of the formula AG(φerror). The authors also define a specification language RCTL, as an extension to the conventional CTL language using regular expressions. More recently, Beer et al. have extended RCTL to include further expressions and syntax that are useful in creating formulas for on-the-fly model checking, as described in “The Temporal Logic Sugar,” Proceedings of the Thirteenth International Conference on Computer Aided Verification (CAV 2001), which is incorporated here in by reference.